The relentless increase in the number of transistors integrated on a single electronic chip has made the traditional method of chip verification using simulation more and more difficult and time-consuming. Desiring additional measures of design confidence, chip developers are increasingly turning to other methods of verification to augment simulation.
Formal verification delivers mathematical proofs of correctness without requiring simulation test bench development. Formal verification processes properties defining intended behavior and makes use of constraints that specify legal input values for the design. Properties can be defined by the chip designer in the form of assertion statements. Properties can also be automatically extracted by electronic design automation (EDA) tools. Automatically extracted properties usually apply to a specific domain such as clock-domain crossing (CDC), power verification, timing exception verification among others. To correctly model the environment of a design, designers specify constraints in SVA/PSL or other standard formats. The constraints are usually referred to as assumptions while the properties to be proved as assertions.
Properties are verified using verification engines. Due to the computational complexity of the verification problem, many verification engines exist and improved verification engines continue to be developed. Different verification engines tackle the verification problem differently to circumvent the computational difficulty of the verification process. Different engines have memory and runtime characteristics that cannot be predicated beforehand. Consequently, it is difficult to predict whether a specific verification engine can prove a specific property or how long it will take. For this reason, engineers want to run multiple verification engines until one succeeds and to be able to limit the computing resources used by each verification engine. In addition, engineers want to be able to quickly integrate state-of-the-art verification engines into their products. Most verification engines process one property at a time.
Baumgartner is an early pioneer in the field of formal verification and in U.S. Pat. Nos. 6,698,003 and 7,266,795 describes a Verification framework that uses multiple specialized engines to decompose a design into smaller pieces, pass information between engines and prove a single property cooperatively. The specialized engines have complex interactions and have no limits on their computation resources.
EDA tools need a framework that can easily incorporate new verification engines with minimal effort, provides ways of composing verification engines so they can run serially and in parallel, with user-specified computing resources.